/*@ nullable_by_default @*/
public interface paircovInterf{
    // GenPre1: All parameter sets are not null.
    //@ requires (\forall int i ; 0<= i && i<params_sets.length; params_sets[i] != null);
    // GenPre2: All parameter sets have at least one element
    //@ requires (\forall int i ; 0<= i && i<params_sets.length; params_sets[i].length > 0);
    // GenPre3: All elements of a parameter set are not null.
    /*@ requires (\forall int i ; 0<= i && i<params_sets.length; 
      @            (\forall int j; 0<= j && j < params_sets[i].length;
      @                                     params_sets[i][j] != null));
      @*/
    // GenPre4: All elements of a parameter set are different.
    /*@ requires (\forall int i ; 0<= i && i<params_sets.length;
      @             (\forall int j ; 0<=j && j<params_sets[i].length;
      @               (\forall int k ; j<k && k<params_sets[i].length;
      @                   !params_sets[i][j].equals(params_sets[i][k]))));
      @*/
    // GenPost1: All testcases of the result have the length of the params_sets
    /*@ ensures (\forall int i; 0<= i && i<\result.length; 
      @              \result[i].get_length() == params_sets.length);
      @*/
    // GenPost2: All testcases only use valid values
    /*@ ensures (\forall int i; 0<= i && i<\result.length;
      @             (\forall int j; 0<= j && j<params_sets.length;
      @                 (\exists int k; 0<= k && k<params_sets[j].length;
      @                     \result[i].get_tc(j).equals(params_sets[j][k]))));
      @*/
    // GenPost3: Each pair is covered
    /*@ ensures (\forall int i;0<= i && i<params_sets.length;
      @            (\forall int j; i< j && j<params_sets.length;
      @       // i and j correspond to two different sets of parameters
      @              (\forall int k; 0<= k && k<params_sets[i].length;
      @                (\forall int l; 0<= l && l<params_sets[j].length;
      @        // k and l correspond to indexes of elements of the two parameter sets
      @                 (\exists int t; 0<=t && t<\result.length;
      @         // t is one test case, where the pair corresponding to k and l exists.
      @                   \result[t].get_tc(i).equals(params_sets[i][k])
      @                     && \result[t].get_tc(j).equals(params_sets[j][l]))))));
      @*/
    public Test_Case [] generate(String [] [] params_sets);
}
